Left Termination of the query pattern
minsort(g,a)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 185 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 173 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
    ↳7 PiDP
        ↳8 UsableRulesProof (⇔, 0 ms)
        ↳9 PiDP
        ↳10 PiDPToQDPProof (⇔, 0 ms)
        ↳11 QDP
        ↳12 QDPSizeChangeProof (⇔, 0 ms)
        ↳13 YES
    ↳14 PiDP
        ↳15 UsableRulesProof (⇔, 0 ms)
        ↳16 PiDP
        ↳17 PiDPToQDPProof (⇒, 0 ms)
        ↳18 QDP
        ↳19 QDPSizeChangeProof (⇔, 0 ms)
        ↳20 YES
    ↳21 PiDP
        ↳22 UsableRulesProof (⇔, 0 ms)
        ↳23 PiDP
        ↳24 PiDPToQDPProof (⇔, 0 ms)
        ↳25 QDP
        ↳26 QDPSizeChangeProof (⇔, 0 ms)
        ↳27 YES
    ↳28 PiDP
        ↳29 UsableRulesProof (⇔, 0 ms)
        ↳30 PiDP
        ↳31 PiDPToQDPProof (⇔, 0 ms)
        ↳32 QDP
        ↳33 QDPSizeChangeProof (⇔, 0 ms)
        ↳34 YES
    ↳35 PiDP
        ↳36 UsableRulesProof (⇔, 0 ms)
        ↳37 PiDP
        ↳38 PiDPToQDPProof (⇒, 0 ms)
        ↳39 QDP
        ↳40 QDPSizeChangeProof (⇔, 0 ms)
        ↳41 YES
    ↳42 PiDP
        ↳43 PiDPToQDPProof (⇒, 29 ms)
        ↳44 QDP
        ↳45 QDPOrderProof (⇔, 407 ms)
        ↳46 QDP
        ↳47 DependencyGraphProof (⇔, 0 ms)
        ↳48 TRUE

(0) Obligation:

Clauses:

minsort([], []).
minsort(L, .(X, L1)) :- ','(min1(X, L), ','(remove(X, L, L2), minsort(L2, L1))).
min1(M, .(X, L)) :- min2(X, M, L).
min2(X, X, []).
min2(X, A, .(M, L)) :- ','(min(X, M, B), min2(B, A, L)).
min(X, Y, X) :- le(X, Y).
min(X, Y, Y) :- gt(X, Y).
remove(N, .(N, L), L).
remove(N, .(M, L), .(M, L1)) :- ','(notEq(N, M), remove(N, L, L1)).
gt(s(X), s(Y)) :- gt(X, Y).
gt(s(X), 0).
le(s(X), s(Y)) :- le(X, Y).
le(0, s(Y)).
le(0, 0).
notEq(s(X), s(Y)) :- notEq(X, Y).
notEq(s(X), 0).
notEq(0, s(X)).

Query: minsort(g,a)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

(2) Obligation:

Triples:

min2A(X1, X2, .(X3, X4)) :- leC(X1, X3).
min2A(X1, X2, .(X3, X4)) :- gtD(X1, X3).
min2A(X1, X2, .(X3, X4)) :- ','(mincB(X1, X3, X5), min2A(X5, X2, X4)).
leC(s(X1), s(X2)) :- leC(X1, X2).
gtD(s(X1), s(X2)) :- gtD(X1, X2).
notEqG(s(X1), s(X2)) :- notEqG(X1, X2).
pH(X1, X2, X3, X4) :- notEqG(X1, X2).
pH(X1, X2, .(X3, X4), .(X3, X5)) :- ','(notEqcG(X1, X2), pH(X1, X3, X4, X5)).
minsortE(.(X1, X2), .(X3, X4)) :- min2A(X1, X3, X2).
minsortE(.(X1, X2), .(X3, X4)) :- ','(min2cA(X1, X3, X2), pH(X3, X1, X2, X5)).
minsortE(.(X1, X2), .(X3, X4)) :- ','(min2cA(X1, X3, X2), ','(removecF(X3, X1, X2, X5), minsortE(X5, X4))).

Clauses:

min2cA(X1, X1, []).
min2cA(X1, X2, .(X3, X4)) :- ','(mincB(X1, X3, X5), min2cA(X5, X2, X4)).
lecC(s(X1), s(X2)) :- lecC(X1, X2).
lecC(0, s(X1)).
lecC(0, 0).
gtcD(s(X1), s(X2)) :- gtcD(X1, X2).
gtcD(s(X1), 0).
minsortcE([], []).
minsortcE(.(X1, X2), .(X3, X4)) :- ','(min2cA(X1, X3, X2), ','(removecF(X3, X1, X2, X5), minsortcE(X5, X4))).
notEqcG(s(X1), s(X2)) :- notEqcG(X1, X2).
notEqcG(s(X1), 0).
notEqcG(0, s(X1)).
qcH(X1, X2, .(X1, X3), X3) :- notEqcG(X1, X2).
qcH(X1, X2, .(X3, X4), .(X3, X5)) :- ','(notEqcG(X1, X2), qcH(X1, X3, X4, X5)).
removecF(X1, X1, X2, X2).
removecF(X1, X2, X3, .(X2, X4)) :- qcH(X1, X2, X3, X4).
mincB(X1, X2, X1) :- lecC(X1, X2).
mincB(X1, X2, X2) :- gtcD(X1, X2).

Afs:

minsortE(x1, x2)  =  minsortE(x1)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
minsortE_in: (b,f)
min2A_in: (b,f,b)
leC_in: (b,b)
gtD_in: (b,b)
mincB_in: (b,b,f)
lecC_in: (b,b)
gtcD_in: (b,b)
min2cA_in: (b,f,b)
pH_in: (b,b,b,f)
notEqG_in: (b,b)
notEqcG_in: (b,b)
removecF_in: (b,b,b,f)
qcH_in: (b,b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

MINSORTE_IN_GA(.(X1, X2), .(X3, X4)) → U11_GA(X1, X2, X3, X4, min2A_in_gag(X1, X3, X2))
MINSORTE_IN_GA(.(X1, X2), .(X3, X4)) → MIN2A_IN_GAG(X1, X3, X2)
MIN2A_IN_GAG(X1, X2, .(X3, X4)) → U1_GAG(X1, X2, X3, X4, leC_in_gg(X1, X3))
MIN2A_IN_GAG(X1, X2, .(X3, X4)) → LEC_IN_GG(X1, X3)
LEC_IN_GG(s(X1), s(X2)) → U5_GG(X1, X2, leC_in_gg(X1, X2))
LEC_IN_GG(s(X1), s(X2)) → LEC_IN_GG(X1, X2)
MIN2A_IN_GAG(X1, X2, .(X3, X4)) → U2_GAG(X1, X2, X3, X4, gtD_in_gg(X1, X3))
MIN2A_IN_GAG(X1, X2, .(X3, X4)) → GTD_IN_GG(X1, X3)
GTD_IN_GG(s(X1), s(X2)) → U6_GG(X1, X2, gtD_in_gg(X1, X2))
GTD_IN_GG(s(X1), s(X2)) → GTD_IN_GG(X1, X2)
MIN2A_IN_GAG(X1, X2, .(X3, X4)) → U3_GAG(X1, X2, X3, X4, mincB_in_gga(X1, X3, X5))
U3_GAG(X1, X2, X3, X4, mincB_out_gga(X1, X3, X5)) → U4_GAG(X1, X2, X3, X4, min2A_in_gag(X5, X2, X4))
U3_GAG(X1, X2, X3, X4, mincB_out_gga(X1, X3, X5)) → MIN2A_IN_GAG(X5, X2, X4)
MINSORTE_IN_GA(.(X1, X2), .(X3, X4)) → U12_GA(X1, X2, X3, X4, min2cA_in_gag(X1, X3, X2))
U12_GA(X1, X2, X3, X4, min2cA_out_gag(X1, X3, X2)) → U13_GA(X1, X2, X3, X4, pH_in_ggga(X3, X1, X2, X5))
U12_GA(X1, X2, X3, X4, min2cA_out_gag(X1, X3, X2)) → PH_IN_GGGA(X3, X1, X2, X5)
PH_IN_GGGA(X1, X2, X3, X4) → U8_GGGA(X1, X2, X3, X4, notEqG_in_gg(X1, X2))
PH_IN_GGGA(X1, X2, X3, X4) → NOTEQG_IN_GG(X1, X2)
NOTEQG_IN_GG(s(X1), s(X2)) → U7_GG(X1, X2, notEqG_in_gg(X1, X2))
NOTEQG_IN_GG(s(X1), s(X2)) → NOTEQG_IN_GG(X1, X2)
PH_IN_GGGA(X1, X2, .(X3, X4), .(X3, X5)) → U9_GGGA(X1, X2, X3, X4, X5, notEqcG_in_gg(X1, X2))
U9_GGGA(X1, X2, X3, X4, X5, notEqcG_out_gg(X1, X2)) → U10_GGGA(X1, X2, X3, X4, X5, pH_in_ggga(X1, X3, X4, X5))
U9_GGGA(X1, X2, X3, X4, X5, notEqcG_out_gg(X1, X2)) → PH_IN_GGGA(X1, X3, X4, X5)
U12_GA(X1, X2, X3, X4, min2cA_out_gag(X1, X3, X2)) → U14_GA(X1, X2, X3, X4, removecF_in_ggga(X3, X1, X2, X5))
U14_GA(X1, X2, X3, X4, removecF_out_ggga(X3, X1, X2, X5)) → U15_GA(X1, X2, X3, X4, minsortE_in_ga(X5, X4))
U14_GA(X1, X2, X3, X4, removecF_out_ggga(X3, X1, X2, X5)) → MINSORTE_IN_GA(X5, X4)

The TRS R consists of the following rules:

mincB_in_gga(X1, X2, X1) → U29_gga(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(s(X1), s(X2)) → U19_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U19_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
U29_gga(X1, X2, lecC_out_gg(X1, X2)) → mincB_out_gga(X1, X2, X1)
mincB_in_gga(X1, X2, X2) → U30_gga(X1, X2, gtcD_in_gg(X1, X2))
gtcD_in_gg(s(X1), s(X2)) → U20_gg(X1, X2, gtcD_in_gg(X1, X2))
gtcD_in_gg(s(X1), 0) → gtcD_out_gg(s(X1), 0)
U20_gg(X1, X2, gtcD_out_gg(X1, X2)) → gtcD_out_gg(s(X1), s(X2))
U30_gga(X1, X2, gtcD_out_gg(X1, X2)) → mincB_out_gga(X1, X2, X2)
min2cA_in_gag(X1, X1, []) → min2cA_out_gag(X1, X1, [])
min2cA_in_gag(X1, X2, .(X3, X4)) → U17_gag(X1, X2, X3, X4, mincB_in_gga(X1, X3, X5))
U17_gag(X1, X2, X3, X4, mincB_out_gga(X1, X3, X5)) → U18_gag(X1, X2, X3, X4, min2cA_in_gag(X5, X2, X4))
U18_gag(X1, X2, X3, X4, min2cA_out_gag(X5, X2, X4)) → min2cA_out_gag(X1, X2, .(X3, X4))
notEqcG_in_gg(s(X1), s(X2)) → U24_gg(X1, X2, notEqcG_in_gg(X1, X2))
notEqcG_in_gg(s(X1), 0) → notEqcG_out_gg(s(X1), 0)
notEqcG_in_gg(0, s(X1)) → notEqcG_out_gg(0, s(X1))
U24_gg(X1, X2, notEqcG_out_gg(X1, X2)) → notEqcG_out_gg(s(X1), s(X2))
removecF_in_ggga(X1, X1, X2, X2) → removecF_out_ggga(X1, X1, X2, X2)
removecF_in_ggga(X1, X2, X3, .(X2, X4)) → U28_ggga(X1, X2, X3, X4, qcH_in_ggga(X1, X2, X3, X4))
qcH_in_ggga(X1, X2, .(X1, X3), X3) → U25_ggga(X1, X2, X3, notEqcG_in_gg(X1, X2))
U25_ggga(X1, X2, X3, notEqcG_out_gg(X1, X2)) → qcH_out_ggga(X1, X2, .(X1, X3), X3)
qcH_in_ggga(X1, X2, .(X3, X4), .(X3, X5)) → U26_ggga(X1, X2, X3, X4, X5, notEqcG_in_gg(X1, X2))
U26_ggga(X1, X2, X3, X4, X5, notEqcG_out_gg(X1, X2)) → U27_ggga(X1, X2, X3, X4, X5, qcH_in_ggga(X1, X3, X4, X5))
U27_ggga(X1, X2, X3, X4, X5, qcH_out_ggga(X1, X3, X4, X5)) → qcH_out_ggga(X1, X2, .(X3, X4), .(X3, X5))
U28_ggga(X1, X2, X3, X4, qcH_out_ggga(X1, X2, X3, X4)) → removecF_out_ggga(X1, X2, X3, .(X2, X4))

The argument filtering Pi contains the following mapping:
minsortE_in_ga(x1, x2)  =  minsortE_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
min2A_in_gag(x1, x2, x3)  =  min2A_in_gag(x1, x3)
leC_in_gg(x1, x2)  =  leC_in_gg(x1, x2)
s(x1)  =  s(x1)
gtD_in_gg(x1, x2)  =  gtD_in_gg(x1, x2)
mincB_in_gga(x1, x2, x3)  =  mincB_in_gga(x1, x2)
U29_gga(x1, x2, x3)  =  U29_gga(x1, x2, x3)
lecC_in_gg(x1, x2)  =  lecC_in_gg(x1, x2)
U19_gg(x1, x2, x3)  =  U19_gg(x1, x2, x3)
0  =  0
lecC_out_gg(x1, x2)  =  lecC_out_gg(x1, x2)
mincB_out_gga(x1, x2, x3)  =  mincB_out_gga(x1, x2, x3)
U30_gga(x1, x2, x3)  =  U30_gga(x1, x2, x3)
gtcD_in_gg(x1, x2)  =  gtcD_in_gg(x1, x2)
U20_gg(x1, x2, x3)  =  U20_gg(x1, x2, x3)
gtcD_out_gg(x1, x2)  =  gtcD_out_gg(x1, x2)
min2cA_in_gag(x1, x2, x3)  =  min2cA_in_gag(x1, x3)
[]  =  []
min2cA_out_gag(x1, x2, x3)  =  min2cA_out_gag(x1, x2, x3)
U17_gag(x1, x2, x3, x4, x5)  =  U17_gag(x1, x3, x4, x5)
U18_gag(x1, x2, x3, x4, x5)  =  U18_gag(x1, x3, x4, x5)
pH_in_ggga(x1, x2, x3, x4)  =  pH_in_ggga(x1, x2, x3)
notEqG_in_gg(x1, x2)  =  notEqG_in_gg(x1, x2)
notEqcG_in_gg(x1, x2)  =  notEqcG_in_gg(x1, x2)
U24_gg(x1, x2, x3)  =  U24_gg(x1, x2, x3)
notEqcG_out_gg(x1, x2)  =  notEqcG_out_gg(x1, x2)
removecF_in_ggga(x1, x2, x3, x4)  =  removecF_in_ggga(x1, x2, x3)
removecF_out_ggga(x1, x2, x3, x4)  =  removecF_out_ggga(x1, x2, x3, x4)
U28_ggga(x1, x2, x3, x4, x5)  =  U28_ggga(x1, x2, x3, x5)
qcH_in_ggga(x1, x2, x3, x4)  =  qcH_in_ggga(x1, x2, x3)
U25_ggga(x1, x2, x3, x4)  =  U25_ggga(x1, x2, x3, x4)
qcH_out_ggga(x1, x2, x3, x4)  =  qcH_out_ggga(x1, x2, x3, x4)
U26_ggga(x1, x2, x3, x4, x5, x6)  =  U26_ggga(x1, x2, x3, x4, x6)
U27_ggga(x1, x2, x3, x4, x5, x6)  =  U27_ggga(x1, x2, x3, x4, x6)
MINSORTE_IN_GA(x1, x2)  =  MINSORTE_IN_GA(x1)
U11_GA(x1, x2, x3, x4, x5)  =  U11_GA(x1, x2, x5)
MIN2A_IN_GAG(x1, x2, x3)  =  MIN2A_IN_GAG(x1, x3)
U1_GAG(x1, x2, x3, x4, x5)  =  U1_GAG(x1, x3, x4, x5)
LEC_IN_GG(x1, x2)  =  LEC_IN_GG(x1, x2)
U5_GG(x1, x2, x3)  =  U5_GG(x1, x2, x3)
U2_GAG(x1, x2, x3, x4, x5)  =  U2_GAG(x1, x3, x4, x5)
GTD_IN_GG(x1, x2)  =  GTD_IN_GG(x1, x2)
U6_GG(x1, x2, x3)  =  U6_GG(x1, x2, x3)
U3_GAG(x1, x2, x3, x4, x5)  =  U3_GAG(x1, x3, x4, x5)
U4_GAG(x1, x2, x3, x4, x5)  =  U4_GAG(x1, x3, x4, x5)
U12_GA(x1, x2, x3, x4, x5)  =  U12_GA(x1, x2, x5)
U13_GA(x1, x2, x3, x4, x5)  =  U13_GA(x1, x2, x5)
PH_IN_GGGA(x1, x2, x3, x4)  =  PH_IN_GGGA(x1, x2, x3)
U8_GGGA(x1, x2, x3, x4, x5)  =  U8_GGGA(x1, x2, x3, x5)
NOTEQG_IN_GG(x1, x2)  =  NOTEQG_IN_GG(x1, x2)
U7_GG(x1, x2, x3)  =  U7_GG(x1, x2, x3)
U9_GGGA(x1, x2, x3, x4, x5, x6)  =  U9_GGGA(x1, x2, x3, x4, x6)
U10_GGGA(x1, x2, x3, x4, x5, x6)  =  U10_GGGA(x1, x2, x3, x4, x6)
U14_GA(x1, x2, x3, x4, x5)  =  U14_GA(x1, x2, x5)
U15_GA(x1, x2, x3, x4, x5)  =  U15_GA(x1, x2, x5)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MINSORTE_IN_GA(.(X1, X2), .(X3, X4)) → U11_GA(X1, X2, X3, X4, min2A_in_gag(X1, X3, X2))
MINSORTE_IN_GA(.(X1, X2), .(X3, X4)) → MIN2A_IN_GAG(X1, X3, X2)
MIN2A_IN_GAG(X1, X2, .(X3, X4)) → U1_GAG(X1, X2, X3, X4, leC_in_gg(X1, X3))
MIN2A_IN_GAG(X1, X2, .(X3, X4)) → LEC_IN_GG(X1, X3)
LEC_IN_GG(s(X1), s(X2)) → U5_GG(X1, X2, leC_in_gg(X1, X2))
LEC_IN_GG(s(X1), s(X2)) → LEC_IN_GG(X1, X2)
MIN2A_IN_GAG(X1, X2, .(X3, X4)) → U2_GAG(X1, X2, X3, X4, gtD_in_gg(X1, X3))
MIN2A_IN_GAG(X1, X2, .(X3, X4)) → GTD_IN_GG(X1, X3)
GTD_IN_GG(s(X1), s(X2)) → U6_GG(X1, X2, gtD_in_gg(X1, X2))
GTD_IN_GG(s(X1), s(X2)) → GTD_IN_GG(X1, X2)
MIN2A_IN_GAG(X1, X2, .(X3, X4)) → U3_GAG(X1, X2, X3, X4, mincB_in_gga(X1, X3, X5))
U3_GAG(X1, X2, X3, X4, mincB_out_gga(X1, X3, X5)) → U4_GAG(X1, X2, X3, X4, min2A_in_gag(X5, X2, X4))
U3_GAG(X1, X2, X3, X4, mincB_out_gga(X1, X3, X5)) → MIN2A_IN_GAG(X5, X2, X4)
MINSORTE_IN_GA(.(X1, X2), .(X3, X4)) → U12_GA(X1, X2, X3, X4, min2cA_in_gag(X1, X3, X2))
U12_GA(X1, X2, X3, X4, min2cA_out_gag(X1, X3, X2)) → U13_GA(X1, X2, X3, X4, pH_in_ggga(X3, X1, X2, X5))
U12_GA(X1, X2, X3, X4, min2cA_out_gag(X1, X3, X2)) → PH_IN_GGGA(X3, X1, X2, X5)
PH_IN_GGGA(X1, X2, X3, X4) → U8_GGGA(X1, X2, X3, X4, notEqG_in_gg(X1, X2))
PH_IN_GGGA(X1, X2, X3, X4) → NOTEQG_IN_GG(X1, X2)
NOTEQG_IN_GG(s(X1), s(X2)) → U7_GG(X1, X2, notEqG_in_gg(X1, X2))
NOTEQG_IN_GG(s(X1), s(X2)) → NOTEQG_IN_GG(X1, X2)
PH_IN_GGGA(X1, X2, .(X3, X4), .(X3, X5)) → U9_GGGA(X1, X2, X3, X4, X5, notEqcG_in_gg(X1, X2))
U9_GGGA(X1, X2, X3, X4, X5, notEqcG_out_gg(X1, X2)) → U10_GGGA(X1, X2, X3, X4, X5, pH_in_ggga(X1, X3, X4, X5))
U9_GGGA(X1, X2, X3, X4, X5, notEqcG_out_gg(X1, X2)) → PH_IN_GGGA(X1, X3, X4, X5)
U12_GA(X1, X2, X3, X4, min2cA_out_gag(X1, X3, X2)) → U14_GA(X1, X2, X3, X4, removecF_in_ggga(X3, X1, X2, X5))
U14_GA(X1, X2, X3, X4, removecF_out_ggga(X3, X1, X2, X5)) → U15_GA(X1, X2, X3, X4, minsortE_in_ga(X5, X4))
U14_GA(X1, X2, X3, X4, removecF_out_ggga(X3, X1, X2, X5)) → MINSORTE_IN_GA(X5, X4)

The TRS R consists of the following rules:

mincB_in_gga(X1, X2, X1) → U29_gga(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(s(X1), s(X2)) → U19_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U19_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
U29_gga(X1, X2, lecC_out_gg(X1, X2)) → mincB_out_gga(X1, X2, X1)
mincB_in_gga(X1, X2, X2) → U30_gga(X1, X2, gtcD_in_gg(X1, X2))
gtcD_in_gg(s(X1), s(X2)) → U20_gg(X1, X2, gtcD_in_gg(X1, X2))
gtcD_in_gg(s(X1), 0) → gtcD_out_gg(s(X1), 0)
U20_gg(X1, X2, gtcD_out_gg(X1, X2)) → gtcD_out_gg(s(X1), s(X2))
U30_gga(X1, X2, gtcD_out_gg(X1, X2)) → mincB_out_gga(X1, X2, X2)
min2cA_in_gag(X1, X1, []) → min2cA_out_gag(X1, X1, [])
min2cA_in_gag(X1, X2, .(X3, X4)) → U17_gag(X1, X2, X3, X4, mincB_in_gga(X1, X3, X5))
U17_gag(X1, X2, X3, X4, mincB_out_gga(X1, X3, X5)) → U18_gag(X1, X2, X3, X4, min2cA_in_gag(X5, X2, X4))
U18_gag(X1, X2, X3, X4, min2cA_out_gag(X5, X2, X4)) → min2cA_out_gag(X1, X2, .(X3, X4))
notEqcG_in_gg(s(X1), s(X2)) → U24_gg(X1, X2, notEqcG_in_gg(X1, X2))
notEqcG_in_gg(s(X1), 0) → notEqcG_out_gg(s(X1), 0)
notEqcG_in_gg(0, s(X1)) → notEqcG_out_gg(0, s(X1))
U24_gg(X1, X2, notEqcG_out_gg(X1, X2)) → notEqcG_out_gg(s(X1), s(X2))
removecF_in_ggga(X1, X1, X2, X2) → removecF_out_ggga(X1, X1, X2, X2)
removecF_in_ggga(X1, X2, X3, .(X2, X4)) → U28_ggga(X1, X2, X3, X4, qcH_in_ggga(X1, X2, X3, X4))
qcH_in_ggga(X1, X2, .(X1, X3), X3) → U25_ggga(X1, X2, X3, notEqcG_in_gg(X1, X2))
U25_ggga(X1, X2, X3, notEqcG_out_gg(X1, X2)) → qcH_out_ggga(X1, X2, .(X1, X3), X3)
qcH_in_ggga(X1, X2, .(X3, X4), .(X3, X5)) → U26_ggga(X1, X2, X3, X4, X5, notEqcG_in_gg(X1, X2))
U26_ggga(X1, X2, X3, X4, X5, notEqcG_out_gg(X1, X2)) → U27_ggga(X1, X2, X3, X4, X5, qcH_in_ggga(X1, X3, X4, X5))
U27_ggga(X1, X2, X3, X4, X5, qcH_out_ggga(X1, X3, X4, X5)) → qcH_out_ggga(X1, X2, .(X3, X4), .(X3, X5))
U28_ggga(X1, X2, X3, X4, qcH_out_ggga(X1, X2, X3, X4)) → removecF_out_ggga(X1, X2, X3, .(X2, X4))

The argument filtering Pi contains the following mapping:
minsortE_in_ga(x1, x2)  =  minsortE_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
min2A_in_gag(x1, x2, x3)  =  min2A_in_gag(x1, x3)
leC_in_gg(x1, x2)  =  leC_in_gg(x1, x2)
s(x1)  =  s(x1)
gtD_in_gg(x1, x2)  =  gtD_in_gg(x1, x2)
mincB_in_gga(x1, x2, x3)  =  mincB_in_gga(x1, x2)
U29_gga(x1, x2, x3)  =  U29_gga(x1, x2, x3)
lecC_in_gg(x1, x2)  =  lecC_in_gg(x1, x2)
U19_gg(x1, x2, x3)  =  U19_gg(x1, x2, x3)
0  =  0
lecC_out_gg(x1, x2)  =  lecC_out_gg(x1, x2)
mincB_out_gga(x1, x2, x3)  =  mincB_out_gga(x1, x2, x3)
U30_gga(x1, x2, x3)  =  U30_gga(x1, x2, x3)
gtcD_in_gg(x1, x2)  =  gtcD_in_gg(x1, x2)
U20_gg(x1, x2, x3)  =  U20_gg(x1, x2, x3)
gtcD_out_gg(x1, x2)  =  gtcD_out_gg(x1, x2)
min2cA_in_gag(x1, x2, x3)  =  min2cA_in_gag(x1, x3)
[]  =  []
min2cA_out_gag(x1, x2, x3)  =  min2cA_out_gag(x1, x2, x3)
U17_gag(x1, x2, x3, x4, x5)  =  U17_gag(x1, x3, x4, x5)
U18_gag(x1, x2, x3, x4, x5)  =  U18_gag(x1, x3, x4, x5)
pH_in_ggga(x1, x2, x3, x4)  =  pH_in_ggga(x1, x2, x3)
notEqG_in_gg(x1, x2)  =  notEqG_in_gg(x1, x2)
notEqcG_in_gg(x1, x2)  =  notEqcG_in_gg(x1, x2)
U24_gg(x1, x2, x3)  =  U24_gg(x1, x2, x3)
notEqcG_out_gg(x1, x2)  =  notEqcG_out_gg(x1, x2)
removecF_in_ggga(x1, x2, x3, x4)  =  removecF_in_ggga(x1, x2, x3)
removecF_out_ggga(x1, x2, x3, x4)  =  removecF_out_ggga(x1, x2, x3, x4)
U28_ggga(x1, x2, x3, x4, x5)  =  U28_ggga(x1, x2, x3, x5)
qcH_in_ggga(x1, x2, x3, x4)  =  qcH_in_ggga(x1, x2, x3)
U25_ggga(x1, x2, x3, x4)  =  U25_ggga(x1, x2, x3, x4)
qcH_out_ggga(x1, x2, x3, x4)  =  qcH_out_ggga(x1, x2, x3, x4)
U26_ggga(x1, x2, x3, x4, x5, x6)  =  U26_ggga(x1, x2, x3, x4, x6)
U27_ggga(x1, x2, x3, x4, x5, x6)  =  U27_ggga(x1, x2, x3, x4, x6)
MINSORTE_IN_GA(x1, x2)  =  MINSORTE_IN_GA(x1)
U11_GA(x1, x2, x3, x4, x5)  =  U11_GA(x1, x2, x5)
MIN2A_IN_GAG(x1, x2, x3)  =  MIN2A_IN_GAG(x1, x3)
U1_GAG(x1, x2, x3, x4, x5)  =  U1_GAG(x1, x3, x4, x5)
LEC_IN_GG(x1, x2)  =  LEC_IN_GG(x1, x2)
U5_GG(x1, x2, x3)  =  U5_GG(x1, x2, x3)
U2_GAG(x1, x2, x3, x4, x5)  =  U2_GAG(x1, x3, x4, x5)
GTD_IN_GG(x1, x2)  =  GTD_IN_GG(x1, x2)
U6_GG(x1, x2, x3)  =  U6_GG(x1, x2, x3)
U3_GAG(x1, x2, x3, x4, x5)  =  U3_GAG(x1, x3, x4, x5)
U4_GAG(x1, x2, x3, x4, x5)  =  U4_GAG(x1, x3, x4, x5)
U12_GA(x1, x2, x3, x4, x5)  =  U12_GA(x1, x2, x5)
U13_GA(x1, x2, x3, x4, x5)  =  U13_GA(x1, x2, x5)
PH_IN_GGGA(x1, x2, x3, x4)  =  PH_IN_GGGA(x1, x2, x3)
U8_GGGA(x1, x2, x3, x4, x5)  =  U8_GGGA(x1, x2, x3, x5)
NOTEQG_IN_GG(x1, x2)  =  NOTEQG_IN_GG(x1, x2)
U7_GG(x1, x2, x3)  =  U7_GG(x1, x2, x3)
U9_GGGA(x1, x2, x3, x4, x5, x6)  =  U9_GGGA(x1, x2, x3, x4, x6)
U10_GGGA(x1, x2, x3, x4, x5, x6)  =  U10_GGGA(x1, x2, x3, x4, x6)
U14_GA(x1, x2, x3, x4, x5)  =  U14_GA(x1, x2, x5)
U15_GA(x1, x2, x3, x4, x5)  =  U15_GA(x1, x2, x5)

We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 6 SCCs with 16 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

NOTEQG_IN_GG(s(X1), s(X2)) → NOTEQG_IN_GG(X1, X2)

The TRS R consists of the following rules:

mincB_in_gga(X1, X2, X1) → U29_gga(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(s(X1), s(X2)) → U19_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U19_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
U29_gga(X1, X2, lecC_out_gg(X1, X2)) → mincB_out_gga(X1, X2, X1)
mincB_in_gga(X1, X2, X2) → U30_gga(X1, X2, gtcD_in_gg(X1, X2))
gtcD_in_gg(s(X1), s(X2)) → U20_gg(X1, X2, gtcD_in_gg(X1, X2))
gtcD_in_gg(s(X1), 0) → gtcD_out_gg(s(X1), 0)
U20_gg(X1, X2, gtcD_out_gg(X1, X2)) → gtcD_out_gg(s(X1), s(X2))
U30_gga(X1, X2, gtcD_out_gg(X1, X2)) → mincB_out_gga(X1, X2, X2)
min2cA_in_gag(X1, X1, []) → min2cA_out_gag(X1, X1, [])
min2cA_in_gag(X1, X2, .(X3, X4)) → U17_gag(X1, X2, X3, X4, mincB_in_gga(X1, X3, X5))
U17_gag(X1, X2, X3, X4, mincB_out_gga(X1, X3, X5)) → U18_gag(X1, X2, X3, X4, min2cA_in_gag(X5, X2, X4))
U18_gag(X1, X2, X3, X4, min2cA_out_gag(X5, X2, X4)) → min2cA_out_gag(X1, X2, .(X3, X4))
notEqcG_in_gg(s(X1), s(X2)) → U24_gg(X1, X2, notEqcG_in_gg(X1, X2))
notEqcG_in_gg(s(X1), 0) → notEqcG_out_gg(s(X1), 0)
notEqcG_in_gg(0, s(X1)) → notEqcG_out_gg(0, s(X1))
U24_gg(X1, X2, notEqcG_out_gg(X1, X2)) → notEqcG_out_gg(s(X1), s(X2))
removecF_in_ggga(X1, X1, X2, X2) → removecF_out_ggga(X1, X1, X2, X2)
removecF_in_ggga(X1, X2, X3, .(X2, X4)) → U28_ggga(X1, X2, X3, X4, qcH_in_ggga(X1, X2, X3, X4))
qcH_in_ggga(X1, X2, .(X1, X3), X3) → U25_ggga(X1, X2, X3, notEqcG_in_gg(X1, X2))
U25_ggga(X1, X2, X3, notEqcG_out_gg(X1, X2)) → qcH_out_ggga(X1, X2, .(X1, X3), X3)
qcH_in_ggga(X1, X2, .(X3, X4), .(X3, X5)) → U26_ggga(X1, X2, X3, X4, X5, notEqcG_in_gg(X1, X2))
U26_ggga(X1, X2, X3, X4, X5, notEqcG_out_gg(X1, X2)) → U27_ggga(X1, X2, X3, X4, X5, qcH_in_ggga(X1, X3, X4, X5))
U27_ggga(X1, X2, X3, X4, X5, qcH_out_ggga(X1, X3, X4, X5)) → qcH_out_ggga(X1, X2, .(X3, X4), .(X3, X5))
U28_ggga(X1, X2, X3, X4, qcH_out_ggga(X1, X2, X3, X4)) → removecF_out_ggga(X1, X2, X3, .(X2, X4))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
mincB_in_gga(x1, x2, x3)  =  mincB_in_gga(x1, x2)
U29_gga(x1, x2, x3)  =  U29_gga(x1, x2, x3)
lecC_in_gg(x1, x2)  =  lecC_in_gg(x1, x2)
U19_gg(x1, x2, x3)  =  U19_gg(x1, x2, x3)
0  =  0
lecC_out_gg(x1, x2)  =  lecC_out_gg(x1, x2)
mincB_out_gga(x1, x2, x3)  =  mincB_out_gga(x1, x2, x3)
U30_gga(x1, x2, x3)  =  U30_gga(x1, x2, x3)
gtcD_in_gg(x1, x2)  =  gtcD_in_gg(x1, x2)
U20_gg(x1, x2, x3)  =  U20_gg(x1, x2, x3)
gtcD_out_gg(x1, x2)  =  gtcD_out_gg(x1, x2)
min2cA_in_gag(x1, x2, x3)  =  min2cA_in_gag(x1, x3)
[]  =  []
min2cA_out_gag(x1, x2, x3)  =  min2cA_out_gag(x1, x2, x3)
U17_gag(x1, x2, x3, x4, x5)  =  U17_gag(x1, x3, x4, x5)
U18_gag(x1, x2, x3, x4, x5)  =  U18_gag(x1, x3, x4, x5)
notEqcG_in_gg(x1, x2)  =  notEqcG_in_gg(x1, x2)
U24_gg(x1, x2, x3)  =  U24_gg(x1, x2, x3)
notEqcG_out_gg(x1, x2)  =  notEqcG_out_gg(x1, x2)
removecF_in_ggga(x1, x2, x3, x4)  =  removecF_in_ggga(x1, x2, x3)
removecF_out_ggga(x1, x2, x3, x4)  =  removecF_out_ggga(x1, x2, x3, x4)
U28_ggga(x1, x2, x3, x4, x5)  =  U28_ggga(x1, x2, x3, x5)
qcH_in_ggga(x1, x2, x3, x4)  =  qcH_in_ggga(x1, x2, x3)
U25_ggga(x1, x2, x3, x4)  =  U25_ggga(x1, x2, x3, x4)
qcH_out_ggga(x1, x2, x3, x4)  =  qcH_out_ggga(x1, x2, x3, x4)
U26_ggga(x1, x2, x3, x4, x5, x6)  =  U26_ggga(x1, x2, x3, x4, x6)
U27_ggga(x1, x2, x3, x4, x5, x6)  =  U27_ggga(x1, x2, x3, x4, x6)
NOTEQG_IN_GG(x1, x2)  =  NOTEQG_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

NOTEQG_IN_GG(s(X1), s(X2)) → NOTEQG_IN_GG(X1, X2)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

(10) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

NOTEQG_IN_GG(s(X1), s(X2)) → NOTEQG_IN_GG(X1, X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • NOTEQG_IN_GG(s(X1), s(X2)) → NOTEQG_IN_GG(X1, X2)
    The graph contains the following edges 1 > 1, 2 > 2

(13) YES

(14) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

PH_IN_GGGA(X1, X2, .(X3, X4), .(X3, X5)) → U9_GGGA(X1, X2, X3, X4, X5, notEqcG_in_gg(X1, X2))
U9_GGGA(X1, X2, X3, X4, X5, notEqcG_out_gg(X1, X2)) → PH_IN_GGGA(X1, X3, X4, X5)

The TRS R consists of the following rules:

mincB_in_gga(X1, X2, X1) → U29_gga(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(s(X1), s(X2)) → U19_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U19_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
U29_gga(X1, X2, lecC_out_gg(X1, X2)) → mincB_out_gga(X1, X2, X1)
mincB_in_gga(X1, X2, X2) → U30_gga(X1, X2, gtcD_in_gg(X1, X2))
gtcD_in_gg(s(X1), s(X2)) → U20_gg(X1, X2, gtcD_in_gg(X1, X2))
gtcD_in_gg(s(X1), 0) → gtcD_out_gg(s(X1), 0)
U20_gg(X1, X2, gtcD_out_gg(X1, X2)) → gtcD_out_gg(s(X1), s(X2))
U30_gga(X1, X2, gtcD_out_gg(X1, X2)) → mincB_out_gga(X1, X2, X2)
min2cA_in_gag(X1, X1, []) → min2cA_out_gag(X1, X1, [])
min2cA_in_gag(X1, X2, .(X3, X4)) → U17_gag(X1, X2, X3, X4, mincB_in_gga(X1, X3, X5))
U17_gag(X1, X2, X3, X4, mincB_out_gga(X1, X3, X5)) → U18_gag(X1, X2, X3, X4, min2cA_in_gag(X5, X2, X4))
U18_gag(X1, X2, X3, X4, min2cA_out_gag(X5, X2, X4)) → min2cA_out_gag(X1, X2, .(X3, X4))
notEqcG_in_gg(s(X1), s(X2)) → U24_gg(X1, X2, notEqcG_in_gg(X1, X2))
notEqcG_in_gg(s(X1), 0) → notEqcG_out_gg(s(X1), 0)
notEqcG_in_gg(0, s(X1)) → notEqcG_out_gg(0, s(X1))
U24_gg(X1, X2, notEqcG_out_gg(X1, X2)) → notEqcG_out_gg(s(X1), s(X2))
removecF_in_ggga(X1, X1, X2, X2) → removecF_out_ggga(X1, X1, X2, X2)
removecF_in_ggga(X1, X2, X3, .(X2, X4)) → U28_ggga(X1, X2, X3, X4, qcH_in_ggga(X1, X2, X3, X4))
qcH_in_ggga(X1, X2, .(X1, X3), X3) → U25_ggga(X1, X2, X3, notEqcG_in_gg(X1, X2))
U25_ggga(X1, X2, X3, notEqcG_out_gg(X1, X2)) → qcH_out_ggga(X1, X2, .(X1, X3), X3)
qcH_in_ggga(X1, X2, .(X3, X4), .(X3, X5)) → U26_ggga(X1, X2, X3, X4, X5, notEqcG_in_gg(X1, X2))
U26_ggga(X1, X2, X3, X4, X5, notEqcG_out_gg(X1, X2)) → U27_ggga(X1, X2, X3, X4, X5, qcH_in_ggga(X1, X3, X4, X5))
U27_ggga(X1, X2, X3, X4, X5, qcH_out_ggga(X1, X3, X4, X5)) → qcH_out_ggga(X1, X2, .(X3, X4), .(X3, X5))
U28_ggga(X1, X2, X3, X4, qcH_out_ggga(X1, X2, X3, X4)) → removecF_out_ggga(X1, X2, X3, .(X2, X4))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
mincB_in_gga(x1, x2, x3)  =  mincB_in_gga(x1, x2)
U29_gga(x1, x2, x3)  =  U29_gga(x1, x2, x3)
lecC_in_gg(x1, x2)  =  lecC_in_gg(x1, x2)
U19_gg(x1, x2, x3)  =  U19_gg(x1, x2, x3)
0  =  0
lecC_out_gg(x1, x2)  =  lecC_out_gg(x1, x2)
mincB_out_gga(x1, x2, x3)  =  mincB_out_gga(x1, x2, x3)
U30_gga(x1, x2, x3)  =  U30_gga(x1, x2, x3)
gtcD_in_gg(x1, x2)  =  gtcD_in_gg(x1, x2)
U20_gg(x1, x2, x3)  =  U20_gg(x1, x2, x3)
gtcD_out_gg(x1, x2)  =  gtcD_out_gg(x1, x2)
min2cA_in_gag(x1, x2, x3)  =  min2cA_in_gag(x1, x3)
[]  =  []
min2cA_out_gag(x1, x2, x3)  =  min2cA_out_gag(x1, x2, x3)
U17_gag(x1, x2, x3, x4, x5)  =  U17_gag(x1, x3, x4, x5)
U18_gag(x1, x2, x3, x4, x5)  =  U18_gag(x1, x3, x4, x5)
notEqcG_in_gg(x1, x2)  =  notEqcG_in_gg(x1, x2)
U24_gg(x1, x2, x3)  =  U24_gg(x1, x2, x3)
notEqcG_out_gg(x1, x2)  =  notEqcG_out_gg(x1, x2)
removecF_in_ggga(x1, x2, x3, x4)  =  removecF_in_ggga(x1, x2, x3)
removecF_out_ggga(x1, x2, x3, x4)  =  removecF_out_ggga(x1, x2, x3, x4)
U28_ggga(x1, x2, x3, x4, x5)  =  U28_ggga(x1, x2, x3, x5)
qcH_in_ggga(x1, x2, x3, x4)  =  qcH_in_ggga(x1, x2, x3)
U25_ggga(x1, x2, x3, x4)  =  U25_ggga(x1, x2, x3, x4)
qcH_out_ggga(x1, x2, x3, x4)  =  qcH_out_ggga(x1, x2, x3, x4)
U26_ggga(x1, x2, x3, x4, x5, x6)  =  U26_ggga(x1, x2, x3, x4, x6)
U27_ggga(x1, x2, x3, x4, x5, x6)  =  U27_ggga(x1, x2, x3, x4, x6)
PH_IN_GGGA(x1, x2, x3, x4)  =  PH_IN_GGGA(x1, x2, x3)
U9_GGGA(x1, x2, x3, x4, x5, x6)  =  U9_GGGA(x1, x2, x3, x4, x6)

We have to consider all (P,R,Pi)-chains

(15) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(16) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

PH_IN_GGGA(X1, X2, .(X3, X4), .(X3, X5)) → U9_GGGA(X1, X2, X3, X4, X5, notEqcG_in_gg(X1, X2))
U9_GGGA(X1, X2, X3, X4, X5, notEqcG_out_gg(X1, X2)) → PH_IN_GGGA(X1, X3, X4, X5)

The TRS R consists of the following rules:

notEqcG_in_gg(s(X1), s(X2)) → U24_gg(X1, X2, notEqcG_in_gg(X1, X2))
notEqcG_in_gg(s(X1), 0) → notEqcG_out_gg(s(X1), 0)
notEqcG_in_gg(0, s(X1)) → notEqcG_out_gg(0, s(X1))
U24_gg(X1, X2, notEqcG_out_gg(X1, X2)) → notEqcG_out_gg(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
0  =  0
notEqcG_in_gg(x1, x2)  =  notEqcG_in_gg(x1, x2)
U24_gg(x1, x2, x3)  =  U24_gg(x1, x2, x3)
notEqcG_out_gg(x1, x2)  =  notEqcG_out_gg(x1, x2)
PH_IN_GGGA(x1, x2, x3, x4)  =  PH_IN_GGGA(x1, x2, x3)
U9_GGGA(x1, x2, x3, x4, x5, x6)  =  U9_GGGA(x1, x2, x3, x4, x6)

We have to consider all (P,R,Pi)-chains

(17) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

PH_IN_GGGA(X1, X2, .(X3, X4)) → U9_GGGA(X1, X2, X3, X4, notEqcG_in_gg(X1, X2))
U9_GGGA(X1, X2, X3, X4, notEqcG_out_gg(X1, X2)) → PH_IN_GGGA(X1, X3, X4)

The TRS R consists of the following rules:

notEqcG_in_gg(s(X1), s(X2)) → U24_gg(X1, X2, notEqcG_in_gg(X1, X2))
notEqcG_in_gg(s(X1), 0) → notEqcG_out_gg(s(X1), 0)
notEqcG_in_gg(0, s(X1)) → notEqcG_out_gg(0, s(X1))
U24_gg(X1, X2, notEqcG_out_gg(X1, X2)) → notEqcG_out_gg(s(X1), s(X2))

The set Q consists of the following terms:

notEqcG_in_gg(x0, x1)
U24_gg(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • U9_GGGA(X1, X2, X3, X4, notEqcG_out_gg(X1, X2)) → PH_IN_GGGA(X1, X3, X4)
    The graph contains the following edges 1 >= 1, 5 > 1, 3 >= 2, 4 >= 3

  • PH_IN_GGGA(X1, X2, .(X3, X4)) → U9_GGGA(X1, X2, X3, X4, notEqcG_in_gg(X1, X2))
    The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 3 > 4

(20) YES

(21) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

GTD_IN_GG(s(X1), s(X2)) → GTD_IN_GG(X1, X2)

The TRS R consists of the following rules:

mincB_in_gga(X1, X2, X1) → U29_gga(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(s(X1), s(X2)) → U19_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U19_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
U29_gga(X1, X2, lecC_out_gg(X1, X2)) → mincB_out_gga(X1, X2, X1)
mincB_in_gga(X1, X2, X2) → U30_gga(X1, X2, gtcD_in_gg(X1, X2))
gtcD_in_gg(s(X1), s(X2)) → U20_gg(X1, X2, gtcD_in_gg(X1, X2))
gtcD_in_gg(s(X1), 0) → gtcD_out_gg(s(X1), 0)
U20_gg(X1, X2, gtcD_out_gg(X1, X2)) → gtcD_out_gg(s(X1), s(X2))
U30_gga(X1, X2, gtcD_out_gg(X1, X2)) → mincB_out_gga(X1, X2, X2)
min2cA_in_gag(X1, X1, []) → min2cA_out_gag(X1, X1, [])
min2cA_in_gag(X1, X2, .(X3, X4)) → U17_gag(X1, X2, X3, X4, mincB_in_gga(X1, X3, X5))
U17_gag(X1, X2, X3, X4, mincB_out_gga(X1, X3, X5)) → U18_gag(X1, X2, X3, X4, min2cA_in_gag(X5, X2, X4))
U18_gag(X1, X2, X3, X4, min2cA_out_gag(X5, X2, X4)) → min2cA_out_gag(X1, X2, .(X3, X4))
notEqcG_in_gg(s(X1), s(X2)) → U24_gg(X1, X2, notEqcG_in_gg(X1, X2))
notEqcG_in_gg(s(X1), 0) → notEqcG_out_gg(s(X1), 0)
notEqcG_in_gg(0, s(X1)) → notEqcG_out_gg(0, s(X1))
U24_gg(X1, X2, notEqcG_out_gg(X1, X2)) → notEqcG_out_gg(s(X1), s(X2))
removecF_in_ggga(X1, X1, X2, X2) → removecF_out_ggga(X1, X1, X2, X2)
removecF_in_ggga(X1, X2, X3, .(X2, X4)) → U28_ggga(X1, X2, X3, X4, qcH_in_ggga(X1, X2, X3, X4))
qcH_in_ggga(X1, X2, .(X1, X3), X3) → U25_ggga(X1, X2, X3, notEqcG_in_gg(X1, X2))
U25_ggga(X1, X2, X3, notEqcG_out_gg(X1, X2)) → qcH_out_ggga(X1, X2, .(X1, X3), X3)
qcH_in_ggga(X1, X2, .(X3, X4), .(X3, X5)) → U26_ggga(X1, X2, X3, X4, X5, notEqcG_in_gg(X1, X2))
U26_ggga(X1, X2, X3, X4, X5, notEqcG_out_gg(X1, X2)) → U27_ggga(X1, X2, X3, X4, X5, qcH_in_ggga(X1, X3, X4, X5))
U27_ggga(X1, X2, X3, X4, X5, qcH_out_ggga(X1, X3, X4, X5)) → qcH_out_ggga(X1, X2, .(X3, X4), .(X3, X5))
U28_ggga(X1, X2, X3, X4, qcH_out_ggga(X1, X2, X3, X4)) → removecF_out_ggga(X1, X2, X3, .(X2, X4))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
mincB_in_gga(x1, x2, x3)  =  mincB_in_gga(x1, x2)
U29_gga(x1, x2, x3)  =  U29_gga(x1, x2, x3)
lecC_in_gg(x1, x2)  =  lecC_in_gg(x1, x2)
U19_gg(x1, x2, x3)  =  U19_gg(x1, x2, x3)
0  =  0
lecC_out_gg(x1, x2)  =  lecC_out_gg(x1, x2)
mincB_out_gga(x1, x2, x3)  =  mincB_out_gga(x1, x2, x3)
U30_gga(x1, x2, x3)  =  U30_gga(x1, x2, x3)
gtcD_in_gg(x1, x2)  =  gtcD_in_gg(x1, x2)
U20_gg(x1, x2, x3)  =  U20_gg(x1, x2, x3)
gtcD_out_gg(x1, x2)  =  gtcD_out_gg(x1, x2)
min2cA_in_gag(x1, x2, x3)  =  min2cA_in_gag(x1, x3)
[]  =  []
min2cA_out_gag(x1, x2, x3)  =  min2cA_out_gag(x1, x2, x3)
U17_gag(x1, x2, x3, x4, x5)  =  U17_gag(x1, x3, x4, x5)
U18_gag(x1, x2, x3, x4, x5)  =  U18_gag(x1, x3, x4, x5)
notEqcG_in_gg(x1, x2)  =  notEqcG_in_gg(x1, x2)
U24_gg(x1, x2, x3)  =  U24_gg(x1, x2, x3)
notEqcG_out_gg(x1, x2)  =  notEqcG_out_gg(x1, x2)
removecF_in_ggga(x1, x2, x3, x4)  =  removecF_in_ggga(x1, x2, x3)
removecF_out_ggga(x1, x2, x3, x4)  =  removecF_out_ggga(x1, x2, x3, x4)
U28_ggga(x1, x2, x3, x4, x5)  =  U28_ggga(x1, x2, x3, x5)
qcH_in_ggga(x1, x2, x3, x4)  =  qcH_in_ggga(x1, x2, x3)
U25_ggga(x1, x2, x3, x4)  =  U25_ggga(x1, x2, x3, x4)
qcH_out_ggga(x1, x2, x3, x4)  =  qcH_out_ggga(x1, x2, x3, x4)
U26_ggga(x1, x2, x3, x4, x5, x6)  =  U26_ggga(x1, x2, x3, x4, x6)
U27_ggga(x1, x2, x3, x4, x5, x6)  =  U27_ggga(x1, x2, x3, x4, x6)
GTD_IN_GG(x1, x2)  =  GTD_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains

(22) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(23) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

GTD_IN_GG(s(X1), s(X2)) → GTD_IN_GG(X1, X2)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

(24) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(25) Obligation:

Q DP problem:
The TRS P consists of the following rules:

GTD_IN_GG(s(X1), s(X2)) → GTD_IN_GG(X1, X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(26) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • GTD_IN_GG(s(X1), s(X2)) → GTD_IN_GG(X1, X2)
    The graph contains the following edges 1 > 1, 2 > 2

(27) YES

(28) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LEC_IN_GG(s(X1), s(X2)) → LEC_IN_GG(X1, X2)

The TRS R consists of the following rules:

mincB_in_gga(X1, X2, X1) → U29_gga(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(s(X1), s(X2)) → U19_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U19_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
U29_gga(X1, X2, lecC_out_gg(X1, X2)) → mincB_out_gga(X1, X2, X1)
mincB_in_gga(X1, X2, X2) → U30_gga(X1, X2, gtcD_in_gg(X1, X2))
gtcD_in_gg(s(X1), s(X2)) → U20_gg(X1, X2, gtcD_in_gg(X1, X2))
gtcD_in_gg(s(X1), 0) → gtcD_out_gg(s(X1), 0)
U20_gg(X1, X2, gtcD_out_gg(X1, X2)) → gtcD_out_gg(s(X1), s(X2))
U30_gga(X1, X2, gtcD_out_gg(X1, X2)) → mincB_out_gga(X1, X2, X2)
min2cA_in_gag(X1, X1, []) → min2cA_out_gag(X1, X1, [])
min2cA_in_gag(X1, X2, .(X3, X4)) → U17_gag(X1, X2, X3, X4, mincB_in_gga(X1, X3, X5))
U17_gag(X1, X2, X3, X4, mincB_out_gga(X1, X3, X5)) → U18_gag(X1, X2, X3, X4, min2cA_in_gag(X5, X2, X4))
U18_gag(X1, X2, X3, X4, min2cA_out_gag(X5, X2, X4)) → min2cA_out_gag(X1, X2, .(X3, X4))
notEqcG_in_gg(s(X1), s(X2)) → U24_gg(X1, X2, notEqcG_in_gg(X1, X2))
notEqcG_in_gg(s(X1), 0) → notEqcG_out_gg(s(X1), 0)
notEqcG_in_gg(0, s(X1)) → notEqcG_out_gg(0, s(X1))
U24_gg(X1, X2, notEqcG_out_gg(X1, X2)) → notEqcG_out_gg(s(X1), s(X2))
removecF_in_ggga(X1, X1, X2, X2) → removecF_out_ggga(X1, X1, X2, X2)
removecF_in_ggga(X1, X2, X3, .(X2, X4)) → U28_ggga(X1, X2, X3, X4, qcH_in_ggga(X1, X2, X3, X4))
qcH_in_ggga(X1, X2, .(X1, X3), X3) → U25_ggga(X1, X2, X3, notEqcG_in_gg(X1, X2))
U25_ggga(X1, X2, X3, notEqcG_out_gg(X1, X2)) → qcH_out_ggga(X1, X2, .(X1, X3), X3)
qcH_in_ggga(X1, X2, .(X3, X4), .(X3, X5)) → U26_ggga(X1, X2, X3, X4, X5, notEqcG_in_gg(X1, X2))
U26_ggga(X1, X2, X3, X4, X5, notEqcG_out_gg(X1, X2)) → U27_ggga(X1, X2, X3, X4, X5, qcH_in_ggga(X1, X3, X4, X5))
U27_ggga(X1, X2, X3, X4, X5, qcH_out_ggga(X1, X3, X4, X5)) → qcH_out_ggga(X1, X2, .(X3, X4), .(X3, X5))
U28_ggga(X1, X2, X3, X4, qcH_out_ggga(X1, X2, X3, X4)) → removecF_out_ggga(X1, X2, X3, .(X2, X4))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
mincB_in_gga(x1, x2, x3)  =  mincB_in_gga(x1, x2)
U29_gga(x1, x2, x3)  =  U29_gga(x1, x2, x3)
lecC_in_gg(x1, x2)  =  lecC_in_gg(x1, x2)
U19_gg(x1, x2, x3)  =  U19_gg(x1, x2, x3)
0  =  0
lecC_out_gg(x1, x2)  =  lecC_out_gg(x1, x2)
mincB_out_gga(x1, x2, x3)  =  mincB_out_gga(x1, x2, x3)
U30_gga(x1, x2, x3)  =  U30_gga(x1, x2, x3)
gtcD_in_gg(x1, x2)  =  gtcD_in_gg(x1, x2)
U20_gg(x1, x2, x3)  =  U20_gg(x1, x2, x3)
gtcD_out_gg(x1, x2)  =  gtcD_out_gg(x1, x2)
min2cA_in_gag(x1, x2, x3)  =  min2cA_in_gag(x1, x3)
[]  =  []
min2cA_out_gag(x1, x2, x3)  =  min2cA_out_gag(x1, x2, x3)
U17_gag(x1, x2, x3, x4, x5)  =  U17_gag(x1, x3, x4, x5)
U18_gag(x1, x2, x3, x4, x5)  =  U18_gag(x1, x3, x4, x5)
notEqcG_in_gg(x1, x2)  =  notEqcG_in_gg(x1, x2)
U24_gg(x1, x2, x3)  =  U24_gg(x1, x2, x3)
notEqcG_out_gg(x1, x2)  =  notEqcG_out_gg(x1, x2)
removecF_in_ggga(x1, x2, x3, x4)  =  removecF_in_ggga(x1, x2, x3)
removecF_out_ggga(x1, x2, x3, x4)  =  removecF_out_ggga(x1, x2, x3, x4)
U28_ggga(x1, x2, x3, x4, x5)  =  U28_ggga(x1, x2, x3, x5)
qcH_in_ggga(x1, x2, x3, x4)  =  qcH_in_ggga(x1, x2, x3)
U25_ggga(x1, x2, x3, x4)  =  U25_ggga(x1, x2, x3, x4)
qcH_out_ggga(x1, x2, x3, x4)  =  qcH_out_ggga(x1, x2, x3, x4)
U26_ggga(x1, x2, x3, x4, x5, x6)  =  U26_ggga(x1, x2, x3, x4, x6)
U27_ggga(x1, x2, x3, x4, x5, x6)  =  U27_ggga(x1, x2, x3, x4, x6)
LEC_IN_GG(x1, x2)  =  LEC_IN_GG(x1, x2)

We have to consider all (P,R,Pi)-chains

(29) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(30) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

LEC_IN_GG(s(X1), s(X2)) → LEC_IN_GG(X1, X2)

R is empty.
Pi is empty.
We have to consider all (P,R,Pi)-chains

(31) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(32) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LEC_IN_GG(s(X1), s(X2)) → LEC_IN_GG(X1, X2)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(33) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • LEC_IN_GG(s(X1), s(X2)) → LEC_IN_GG(X1, X2)
    The graph contains the following edges 1 > 1, 2 > 2

(34) YES

(35) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MIN2A_IN_GAG(X1, X2, .(X3, X4)) → U3_GAG(X1, X2, X3, X4, mincB_in_gga(X1, X3, X5))
U3_GAG(X1, X2, X3, X4, mincB_out_gga(X1, X3, X5)) → MIN2A_IN_GAG(X5, X2, X4)

The TRS R consists of the following rules:

mincB_in_gga(X1, X2, X1) → U29_gga(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(s(X1), s(X2)) → U19_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U19_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
U29_gga(X1, X2, lecC_out_gg(X1, X2)) → mincB_out_gga(X1, X2, X1)
mincB_in_gga(X1, X2, X2) → U30_gga(X1, X2, gtcD_in_gg(X1, X2))
gtcD_in_gg(s(X1), s(X2)) → U20_gg(X1, X2, gtcD_in_gg(X1, X2))
gtcD_in_gg(s(X1), 0) → gtcD_out_gg(s(X1), 0)
U20_gg(X1, X2, gtcD_out_gg(X1, X2)) → gtcD_out_gg(s(X1), s(X2))
U30_gga(X1, X2, gtcD_out_gg(X1, X2)) → mincB_out_gga(X1, X2, X2)
min2cA_in_gag(X1, X1, []) → min2cA_out_gag(X1, X1, [])
min2cA_in_gag(X1, X2, .(X3, X4)) → U17_gag(X1, X2, X3, X4, mincB_in_gga(X1, X3, X5))
U17_gag(X1, X2, X3, X4, mincB_out_gga(X1, X3, X5)) → U18_gag(X1, X2, X3, X4, min2cA_in_gag(X5, X2, X4))
U18_gag(X1, X2, X3, X4, min2cA_out_gag(X5, X2, X4)) → min2cA_out_gag(X1, X2, .(X3, X4))
notEqcG_in_gg(s(X1), s(X2)) → U24_gg(X1, X2, notEqcG_in_gg(X1, X2))
notEqcG_in_gg(s(X1), 0) → notEqcG_out_gg(s(X1), 0)
notEqcG_in_gg(0, s(X1)) → notEqcG_out_gg(0, s(X1))
U24_gg(X1, X2, notEqcG_out_gg(X1, X2)) → notEqcG_out_gg(s(X1), s(X2))
removecF_in_ggga(X1, X1, X2, X2) → removecF_out_ggga(X1, X1, X2, X2)
removecF_in_ggga(X1, X2, X3, .(X2, X4)) → U28_ggga(X1, X2, X3, X4, qcH_in_ggga(X1, X2, X3, X4))
qcH_in_ggga(X1, X2, .(X1, X3), X3) → U25_ggga(X1, X2, X3, notEqcG_in_gg(X1, X2))
U25_ggga(X1, X2, X3, notEqcG_out_gg(X1, X2)) → qcH_out_ggga(X1, X2, .(X1, X3), X3)
qcH_in_ggga(X1, X2, .(X3, X4), .(X3, X5)) → U26_ggga(X1, X2, X3, X4, X5, notEqcG_in_gg(X1, X2))
U26_ggga(X1, X2, X3, X4, X5, notEqcG_out_gg(X1, X2)) → U27_ggga(X1, X2, X3, X4, X5, qcH_in_ggga(X1, X3, X4, X5))
U27_ggga(X1, X2, X3, X4, X5, qcH_out_ggga(X1, X3, X4, X5)) → qcH_out_ggga(X1, X2, .(X3, X4), .(X3, X5))
U28_ggga(X1, X2, X3, X4, qcH_out_ggga(X1, X2, X3, X4)) → removecF_out_ggga(X1, X2, X3, .(X2, X4))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
mincB_in_gga(x1, x2, x3)  =  mincB_in_gga(x1, x2)
U29_gga(x1, x2, x3)  =  U29_gga(x1, x2, x3)
lecC_in_gg(x1, x2)  =  lecC_in_gg(x1, x2)
U19_gg(x1, x2, x3)  =  U19_gg(x1, x2, x3)
0  =  0
lecC_out_gg(x1, x2)  =  lecC_out_gg(x1, x2)
mincB_out_gga(x1, x2, x3)  =  mincB_out_gga(x1, x2, x3)
U30_gga(x1, x2, x3)  =  U30_gga(x1, x2, x3)
gtcD_in_gg(x1, x2)  =  gtcD_in_gg(x1, x2)
U20_gg(x1, x2, x3)  =  U20_gg(x1, x2, x3)
gtcD_out_gg(x1, x2)  =  gtcD_out_gg(x1, x2)
min2cA_in_gag(x1, x2, x3)  =  min2cA_in_gag(x1, x3)
[]  =  []
min2cA_out_gag(x1, x2, x3)  =  min2cA_out_gag(x1, x2, x3)
U17_gag(x1, x2, x3, x4, x5)  =  U17_gag(x1, x3, x4, x5)
U18_gag(x1, x2, x3, x4, x5)  =  U18_gag(x1, x3, x4, x5)
notEqcG_in_gg(x1, x2)  =  notEqcG_in_gg(x1, x2)
U24_gg(x1, x2, x3)  =  U24_gg(x1, x2, x3)
notEqcG_out_gg(x1, x2)  =  notEqcG_out_gg(x1, x2)
removecF_in_ggga(x1, x2, x3, x4)  =  removecF_in_ggga(x1, x2, x3)
removecF_out_ggga(x1, x2, x3, x4)  =  removecF_out_ggga(x1, x2, x3, x4)
U28_ggga(x1, x2, x3, x4, x5)  =  U28_ggga(x1, x2, x3, x5)
qcH_in_ggga(x1, x2, x3, x4)  =  qcH_in_ggga(x1, x2, x3)
U25_ggga(x1, x2, x3, x4)  =  U25_ggga(x1, x2, x3, x4)
qcH_out_ggga(x1, x2, x3, x4)  =  qcH_out_ggga(x1, x2, x3, x4)
U26_ggga(x1, x2, x3, x4, x5, x6)  =  U26_ggga(x1, x2, x3, x4, x6)
U27_ggga(x1, x2, x3, x4, x5, x6)  =  U27_ggga(x1, x2, x3, x4, x6)
MIN2A_IN_GAG(x1, x2, x3)  =  MIN2A_IN_GAG(x1, x3)
U3_GAG(x1, x2, x3, x4, x5)  =  U3_GAG(x1, x3, x4, x5)

We have to consider all (P,R,Pi)-chains

(36) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(37) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MIN2A_IN_GAG(X1, X2, .(X3, X4)) → U3_GAG(X1, X2, X3, X4, mincB_in_gga(X1, X3, X5))
U3_GAG(X1, X2, X3, X4, mincB_out_gga(X1, X3, X5)) → MIN2A_IN_GAG(X5, X2, X4)

The TRS R consists of the following rules:

mincB_in_gga(X1, X2, X1) → U29_gga(X1, X2, lecC_in_gg(X1, X2))
mincB_in_gga(X1, X2, X2) → U30_gga(X1, X2, gtcD_in_gg(X1, X2))
U29_gga(X1, X2, lecC_out_gg(X1, X2)) → mincB_out_gga(X1, X2, X1)
U30_gga(X1, X2, gtcD_out_gg(X1, X2)) → mincB_out_gga(X1, X2, X2)
lecC_in_gg(s(X1), s(X2)) → U19_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
gtcD_in_gg(s(X1), s(X2)) → U20_gg(X1, X2, gtcD_in_gg(X1, X2))
gtcD_in_gg(s(X1), 0) → gtcD_out_gg(s(X1), 0)
U19_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
U20_gg(X1, X2, gtcD_out_gg(X1, X2)) → gtcD_out_gg(s(X1), s(X2))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
mincB_in_gga(x1, x2, x3)  =  mincB_in_gga(x1, x2)
U29_gga(x1, x2, x3)  =  U29_gga(x1, x2, x3)
lecC_in_gg(x1, x2)  =  lecC_in_gg(x1, x2)
U19_gg(x1, x2, x3)  =  U19_gg(x1, x2, x3)
0  =  0
lecC_out_gg(x1, x2)  =  lecC_out_gg(x1, x2)
mincB_out_gga(x1, x2, x3)  =  mincB_out_gga(x1, x2, x3)
U30_gga(x1, x2, x3)  =  U30_gga(x1, x2, x3)
gtcD_in_gg(x1, x2)  =  gtcD_in_gg(x1, x2)
U20_gg(x1, x2, x3)  =  U20_gg(x1, x2, x3)
gtcD_out_gg(x1, x2)  =  gtcD_out_gg(x1, x2)
MIN2A_IN_GAG(x1, x2, x3)  =  MIN2A_IN_GAG(x1, x3)
U3_GAG(x1, x2, x3, x4, x5)  =  U3_GAG(x1, x3, x4, x5)

We have to consider all (P,R,Pi)-chains

(38) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(39) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MIN2A_IN_GAG(X1, .(X3, X4)) → U3_GAG(X1, X3, X4, mincB_in_gga(X1, X3))
U3_GAG(X1, X3, X4, mincB_out_gga(X1, X3, X5)) → MIN2A_IN_GAG(X5, X4)

The TRS R consists of the following rules:

mincB_in_gga(X1, X2) → U29_gga(X1, X2, lecC_in_gg(X1, X2))
mincB_in_gga(X1, X2) → U30_gga(X1, X2, gtcD_in_gg(X1, X2))
U29_gga(X1, X2, lecC_out_gg(X1, X2)) → mincB_out_gga(X1, X2, X1)
U30_gga(X1, X2, gtcD_out_gg(X1, X2)) → mincB_out_gga(X1, X2, X2)
lecC_in_gg(s(X1), s(X2)) → U19_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
gtcD_in_gg(s(X1), s(X2)) → U20_gg(X1, X2, gtcD_in_gg(X1, X2))
gtcD_in_gg(s(X1), 0) → gtcD_out_gg(s(X1), 0)
U19_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
U20_gg(X1, X2, gtcD_out_gg(X1, X2)) → gtcD_out_gg(s(X1), s(X2))

The set Q consists of the following terms:

mincB_in_gga(x0, x1)
U29_gga(x0, x1, x2)
U30_gga(x0, x1, x2)
lecC_in_gg(x0, x1)
gtcD_in_gg(x0, x1)
U19_gg(x0, x1, x2)
U20_gg(x0, x1, x2)

We have to consider all (P,Q,R)-chains.

(40) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • U3_GAG(X1, X3, X4, mincB_out_gga(X1, X3, X5)) → MIN2A_IN_GAG(X5, X4)
    The graph contains the following edges 4 > 1, 3 >= 2

  • MIN2A_IN_GAG(X1, .(X3, X4)) → U3_GAG(X1, X3, X4, mincB_in_gga(X1, X3))
    The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3

(41) YES

(42) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MINSORTE_IN_GA(.(X1, X2), .(X3, X4)) → U12_GA(X1, X2, X3, X4, min2cA_in_gag(X1, X3, X2))
U12_GA(X1, X2, X3, X4, min2cA_out_gag(X1, X3, X2)) → U14_GA(X1, X2, X3, X4, removecF_in_ggga(X3, X1, X2, X5))
U14_GA(X1, X2, X3, X4, removecF_out_ggga(X3, X1, X2, X5)) → MINSORTE_IN_GA(X5, X4)

The TRS R consists of the following rules:

mincB_in_gga(X1, X2, X1) → U29_gga(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(s(X1), s(X2)) → U19_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U19_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
U29_gga(X1, X2, lecC_out_gg(X1, X2)) → mincB_out_gga(X1, X2, X1)
mincB_in_gga(X1, X2, X2) → U30_gga(X1, X2, gtcD_in_gg(X1, X2))
gtcD_in_gg(s(X1), s(X2)) → U20_gg(X1, X2, gtcD_in_gg(X1, X2))
gtcD_in_gg(s(X1), 0) → gtcD_out_gg(s(X1), 0)
U20_gg(X1, X2, gtcD_out_gg(X1, X2)) → gtcD_out_gg(s(X1), s(X2))
U30_gga(X1, X2, gtcD_out_gg(X1, X2)) → mincB_out_gga(X1, X2, X2)
min2cA_in_gag(X1, X1, []) → min2cA_out_gag(X1, X1, [])
min2cA_in_gag(X1, X2, .(X3, X4)) → U17_gag(X1, X2, X3, X4, mincB_in_gga(X1, X3, X5))
U17_gag(X1, X2, X3, X4, mincB_out_gga(X1, X3, X5)) → U18_gag(X1, X2, X3, X4, min2cA_in_gag(X5, X2, X4))
U18_gag(X1, X2, X3, X4, min2cA_out_gag(X5, X2, X4)) → min2cA_out_gag(X1, X2, .(X3, X4))
notEqcG_in_gg(s(X1), s(X2)) → U24_gg(X1, X2, notEqcG_in_gg(X1, X2))
notEqcG_in_gg(s(X1), 0) → notEqcG_out_gg(s(X1), 0)
notEqcG_in_gg(0, s(X1)) → notEqcG_out_gg(0, s(X1))
U24_gg(X1, X2, notEqcG_out_gg(X1, X2)) → notEqcG_out_gg(s(X1), s(X2))
removecF_in_ggga(X1, X1, X2, X2) → removecF_out_ggga(X1, X1, X2, X2)
removecF_in_ggga(X1, X2, X3, .(X2, X4)) → U28_ggga(X1, X2, X3, X4, qcH_in_ggga(X1, X2, X3, X4))
qcH_in_ggga(X1, X2, .(X1, X3), X3) → U25_ggga(X1, X2, X3, notEqcG_in_gg(X1, X2))
U25_ggga(X1, X2, X3, notEqcG_out_gg(X1, X2)) → qcH_out_ggga(X1, X2, .(X1, X3), X3)
qcH_in_ggga(X1, X2, .(X3, X4), .(X3, X5)) → U26_ggga(X1, X2, X3, X4, X5, notEqcG_in_gg(X1, X2))
U26_ggga(X1, X2, X3, X4, X5, notEqcG_out_gg(X1, X2)) → U27_ggga(X1, X2, X3, X4, X5, qcH_in_ggga(X1, X3, X4, X5))
U27_ggga(X1, X2, X3, X4, X5, qcH_out_ggga(X1, X3, X4, X5)) → qcH_out_ggga(X1, X2, .(X3, X4), .(X3, X5))
U28_ggga(X1, X2, X3, X4, qcH_out_ggga(X1, X2, X3, X4)) → removecF_out_ggga(X1, X2, X3, .(X2, X4))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
mincB_in_gga(x1, x2, x3)  =  mincB_in_gga(x1, x2)
U29_gga(x1, x2, x3)  =  U29_gga(x1, x2, x3)
lecC_in_gg(x1, x2)  =  lecC_in_gg(x1, x2)
U19_gg(x1, x2, x3)  =  U19_gg(x1, x2, x3)
0  =  0
lecC_out_gg(x1, x2)  =  lecC_out_gg(x1, x2)
mincB_out_gga(x1, x2, x3)  =  mincB_out_gga(x1, x2, x3)
U30_gga(x1, x2, x3)  =  U30_gga(x1, x2, x3)
gtcD_in_gg(x1, x2)  =  gtcD_in_gg(x1, x2)
U20_gg(x1, x2, x3)  =  U20_gg(x1, x2, x3)
gtcD_out_gg(x1, x2)  =  gtcD_out_gg(x1, x2)
min2cA_in_gag(x1, x2, x3)  =  min2cA_in_gag(x1, x3)
[]  =  []
min2cA_out_gag(x1, x2, x3)  =  min2cA_out_gag(x1, x2, x3)
U17_gag(x1, x2, x3, x4, x5)  =  U17_gag(x1, x3, x4, x5)
U18_gag(x1, x2, x3, x4, x5)  =  U18_gag(x1, x3, x4, x5)
notEqcG_in_gg(x1, x2)  =  notEqcG_in_gg(x1, x2)
U24_gg(x1, x2, x3)  =  U24_gg(x1, x2, x3)
notEqcG_out_gg(x1, x2)  =  notEqcG_out_gg(x1, x2)
removecF_in_ggga(x1, x2, x3, x4)  =  removecF_in_ggga(x1, x2, x3)
removecF_out_ggga(x1, x2, x3, x4)  =  removecF_out_ggga(x1, x2, x3, x4)
U28_ggga(x1, x2, x3, x4, x5)  =  U28_ggga(x1, x2, x3, x5)
qcH_in_ggga(x1, x2, x3, x4)  =  qcH_in_ggga(x1, x2, x3)
U25_ggga(x1, x2, x3, x4)  =  U25_ggga(x1, x2, x3, x4)
qcH_out_ggga(x1, x2, x3, x4)  =  qcH_out_ggga(x1, x2, x3, x4)
U26_ggga(x1, x2, x3, x4, x5, x6)  =  U26_ggga(x1, x2, x3, x4, x6)
U27_ggga(x1, x2, x3, x4, x5, x6)  =  U27_ggga(x1, x2, x3, x4, x6)
MINSORTE_IN_GA(x1, x2)  =  MINSORTE_IN_GA(x1)
U12_GA(x1, x2, x3, x4, x5)  =  U12_GA(x1, x2, x5)
U14_GA(x1, x2, x3, x4, x5)  =  U14_GA(x1, x2, x5)

We have to consider all (P,R,Pi)-chains

(43) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(44) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MINSORTE_IN_GA(.(X1, X2)) → U12_GA(X1, X2, min2cA_in_gag(X1, X2))
U12_GA(X1, X2, min2cA_out_gag(X1, X3, X2)) → U14_GA(X1, X2, removecF_in_ggga(X3, X1, X2))
U14_GA(X1, X2, removecF_out_ggga(X3, X1, X2, X5)) → MINSORTE_IN_GA(X5)

The TRS R consists of the following rules:

mincB_in_gga(X1, X2) → U29_gga(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(s(X1), s(X2)) → U19_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U19_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
U29_gga(X1, X2, lecC_out_gg(X1, X2)) → mincB_out_gga(X1, X2, X1)
mincB_in_gga(X1, X2) → U30_gga(X1, X2, gtcD_in_gg(X1, X2))
gtcD_in_gg(s(X1), s(X2)) → U20_gg(X1, X2, gtcD_in_gg(X1, X2))
gtcD_in_gg(s(X1), 0) → gtcD_out_gg(s(X1), 0)
U20_gg(X1, X2, gtcD_out_gg(X1, X2)) → gtcD_out_gg(s(X1), s(X2))
U30_gga(X1, X2, gtcD_out_gg(X1, X2)) → mincB_out_gga(X1, X2, X2)
min2cA_in_gag(X1, []) → min2cA_out_gag(X1, X1, [])
min2cA_in_gag(X1, .(X3, X4)) → U17_gag(X1, X3, X4, mincB_in_gga(X1, X3))
U17_gag(X1, X3, X4, mincB_out_gga(X1, X3, X5)) → U18_gag(X1, X3, X4, min2cA_in_gag(X5, X4))
U18_gag(X1, X3, X4, min2cA_out_gag(X5, X2, X4)) → min2cA_out_gag(X1, X2, .(X3, X4))
notEqcG_in_gg(s(X1), s(X2)) → U24_gg(X1, X2, notEqcG_in_gg(X1, X2))
notEqcG_in_gg(s(X1), 0) → notEqcG_out_gg(s(X1), 0)
notEqcG_in_gg(0, s(X1)) → notEqcG_out_gg(0, s(X1))
U24_gg(X1, X2, notEqcG_out_gg(X1, X2)) → notEqcG_out_gg(s(X1), s(X2))
removecF_in_ggga(X1, X1, X2) → removecF_out_ggga(X1, X1, X2, X2)
removecF_in_ggga(X1, X2, X3) → U28_ggga(X1, X2, X3, qcH_in_ggga(X1, X2, X3))
qcH_in_ggga(X1, X2, .(X1, X3)) → U25_ggga(X1, X2, X3, notEqcG_in_gg(X1, X2))
U25_ggga(X1, X2, X3, notEqcG_out_gg(X1, X2)) → qcH_out_ggga(X1, X2, .(X1, X3), X3)
qcH_in_ggga(X1, X2, .(X3, X4)) → U26_ggga(X1, X2, X3, X4, notEqcG_in_gg(X1, X2))
U26_ggga(X1, X2, X3, X4, notEqcG_out_gg(X1, X2)) → U27_ggga(X1, X2, X3, X4, qcH_in_ggga(X1, X3, X4))
U27_ggga(X1, X2, X3, X4, qcH_out_ggga(X1, X3, X4, X5)) → qcH_out_ggga(X1, X2, .(X3, X4), .(X3, X5))
U28_ggga(X1, X2, X3, qcH_out_ggga(X1, X2, X3, X4)) → removecF_out_ggga(X1, X2, X3, .(X2, X4))

The set Q consists of the following terms:

mincB_in_gga(x0, x1)
lecC_in_gg(x0, x1)
U19_gg(x0, x1, x2)
U29_gga(x0, x1, x2)
gtcD_in_gg(x0, x1)
U20_gg(x0, x1, x2)
U30_gga(x0, x1, x2)
min2cA_in_gag(x0, x1)
U17_gag(x0, x1, x2, x3)
U18_gag(x0, x1, x2, x3)
notEqcG_in_gg(x0, x1)
U24_gg(x0, x1, x2)
removecF_in_ggga(x0, x1, x2)
qcH_in_ggga(x0, x1, x2)
U25_ggga(x0, x1, x2, x3)
U26_ggga(x0, x1, x2, x3, x4)
U27_ggga(x0, x1, x2, x3, x4)
U28_ggga(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.

(45) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


MINSORTE_IN_GA(.(X1, X2)) → U12_GA(X1, X2, min2cA_in_gag(X1, X2))
U12_GA(X1, X2, min2cA_out_gag(X1, X3, X2)) → U14_GA(X1, X2, removecF_in_ggga(X3, X1, X2))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:

POL( U12_GA(x1, ..., x3) ) = 2x2 + 1


POL( min2cA_in_gag(x1, x2) ) = 0


POL( [] ) = 0


POL( min2cA_out_gag(x1, ..., x3) ) = 2


POL( .(x1, x2) ) = 2x2 + 1


POL( U17_gag(x1, ..., x4) ) = max{0, x1 - 2}


POL( mincB_in_gga(x1, x2) ) = x1 + 1


POL( U14_GA(x1, ..., x3) ) = 2x3


POL( removecF_in_ggga(x1, ..., x3) ) = x3


POL( removecF_out_ggga(x1, ..., x4) ) = x4


POL( U28_ggga(x1, ..., x4) ) = x4


POL( qcH_in_ggga(x1, ..., x3) ) = x3


POL( mincB_out_gga(x1, ..., x3) ) = 2


POL( U18_gag(x1, ..., x4) ) = 2x1 + x2 + x3 + 2


POL( U29_gga(x1, ..., x3) ) = 2x1 + 2x2 + 1


POL( lecC_in_gg(x1, x2) ) = 0


POL( U30_gga(x1, ..., x3) ) = x1 + x2 + 2x3 + 2


POL( gtcD_in_gg(x1, x2) ) = x1


POL( s(x1) ) = x1 + 1


POL( U19_gg(x1, ..., x3) ) = max{0, -2}


POL( 0 ) = 0


POL( lecC_out_gg(x1, x2) ) = max{0, x2 - 2}


POL( U20_gg(x1, ..., x3) ) = max{0, x2 - 2}


POL( gtcD_out_gg(x1, x2) ) = 2x1 + 2


POL( U25_ggga(x1, ..., x4) ) = 2x3 + 1


POL( notEqcG_in_gg(x1, x2) ) = 2x2


POL( U26_ggga(x1, ..., x5) ) = 2x4 + 1


POL( qcH_out_ggga(x1, ..., x4) ) = 2x4 + 1


POL( U24_gg(x1, ..., x3) ) = 2


POL( notEqcG_out_gg(x1, x2) ) = max{0, 2x2 - 2}


POL( U27_ggga(x1, ..., x5) ) = 2x5 + 1


POL( MINSORTE_IN_GA(x1) ) = 2x1



The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

removecF_in_ggga(X1, X1, X2) → removecF_out_ggga(X1, X1, X2, X2)
removecF_in_ggga(X1, X2, X3) → U28_ggga(X1, X2, X3, qcH_in_ggga(X1, X2, X3))
qcH_in_ggga(X1, X2, .(X1, X3)) → U25_ggga(X1, X2, X3, notEqcG_in_gg(X1, X2))
qcH_in_ggga(X1, X2, .(X3, X4)) → U26_ggga(X1, X2, X3, X4, notEqcG_in_gg(X1, X2))
U28_ggga(X1, X2, X3, qcH_out_ggga(X1, X2, X3, X4)) → removecF_out_ggga(X1, X2, X3, .(X2, X4))
U26_ggga(X1, X2, X3, X4, notEqcG_out_gg(X1, X2)) → U27_ggga(X1, X2, X3, X4, qcH_in_ggga(X1, X3, X4))
U27_ggga(X1, X2, X3, X4, qcH_out_ggga(X1, X3, X4, X5)) → qcH_out_ggga(X1, X2, .(X3, X4), .(X3, X5))
U25_ggga(X1, X2, X3, notEqcG_out_gg(X1, X2)) → qcH_out_ggga(X1, X2, .(X1, X3), X3)

(46) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U14_GA(X1, X2, removecF_out_ggga(X3, X1, X2, X5)) → MINSORTE_IN_GA(X5)

The TRS R consists of the following rules:

mincB_in_gga(X1, X2) → U29_gga(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(s(X1), s(X2)) → U19_gg(X1, X2, lecC_in_gg(X1, X2))
lecC_in_gg(0, s(X1)) → lecC_out_gg(0, s(X1))
lecC_in_gg(0, 0) → lecC_out_gg(0, 0)
U19_gg(X1, X2, lecC_out_gg(X1, X2)) → lecC_out_gg(s(X1), s(X2))
U29_gga(X1, X2, lecC_out_gg(X1, X2)) → mincB_out_gga(X1, X2, X1)
mincB_in_gga(X1, X2) → U30_gga(X1, X2, gtcD_in_gg(X1, X2))
gtcD_in_gg(s(X1), s(X2)) → U20_gg(X1, X2, gtcD_in_gg(X1, X2))
gtcD_in_gg(s(X1), 0) → gtcD_out_gg(s(X1), 0)
U20_gg(X1, X2, gtcD_out_gg(X1, X2)) → gtcD_out_gg(s(X1), s(X2))
U30_gga(X1, X2, gtcD_out_gg(X1, X2)) → mincB_out_gga(X1, X2, X2)
min2cA_in_gag(X1, []) → min2cA_out_gag(X1, X1, [])
min2cA_in_gag(X1, .(X3, X4)) → U17_gag(X1, X3, X4, mincB_in_gga(X1, X3))
U17_gag(X1, X3, X4, mincB_out_gga(X1, X3, X5)) → U18_gag(X1, X3, X4, min2cA_in_gag(X5, X4))
U18_gag(X1, X3, X4, min2cA_out_gag(X5, X2, X4)) → min2cA_out_gag(X1, X2, .(X3, X4))
notEqcG_in_gg(s(X1), s(X2)) → U24_gg(X1, X2, notEqcG_in_gg(X1, X2))
notEqcG_in_gg(s(X1), 0) → notEqcG_out_gg(s(X1), 0)
notEqcG_in_gg(0, s(X1)) → notEqcG_out_gg(0, s(X1))
U24_gg(X1, X2, notEqcG_out_gg(X1, X2)) → notEqcG_out_gg(s(X1), s(X2))
removecF_in_ggga(X1, X1, X2) → removecF_out_ggga(X1, X1, X2, X2)
removecF_in_ggga(X1, X2, X3) → U28_ggga(X1, X2, X3, qcH_in_ggga(X1, X2, X3))
qcH_in_ggga(X1, X2, .(X1, X3)) → U25_ggga(X1, X2, X3, notEqcG_in_gg(X1, X2))
U25_ggga(X1, X2, X3, notEqcG_out_gg(X1, X2)) → qcH_out_ggga(X1, X2, .(X1, X3), X3)
qcH_in_ggga(X1, X2, .(X3, X4)) → U26_ggga(X1, X2, X3, X4, notEqcG_in_gg(X1, X2))
U26_ggga(X1, X2, X3, X4, notEqcG_out_gg(X1, X2)) → U27_ggga(X1, X2, X3, X4, qcH_in_ggga(X1, X3, X4))
U27_ggga(X1, X2, X3, X4, qcH_out_ggga(X1, X3, X4, X5)) → qcH_out_ggga(X1, X2, .(X3, X4), .(X3, X5))
U28_ggga(X1, X2, X3, qcH_out_ggga(X1, X2, X3, X4)) → removecF_out_ggga(X1, X2, X3, .(X2, X4))

The set Q consists of the following terms:

mincB_in_gga(x0, x1)
lecC_in_gg(x0, x1)
U19_gg(x0, x1, x2)
U29_gga(x0, x1, x2)
gtcD_in_gg(x0, x1)
U20_gg(x0, x1, x2)
U30_gga(x0, x1, x2)
min2cA_in_gag(x0, x1)
U17_gag(x0, x1, x2, x3)
U18_gag(x0, x1, x2, x3)
notEqcG_in_gg(x0, x1)
U24_gg(x0, x1, x2)
removecF_in_ggga(x0, x1, x2)
qcH_in_ggga(x0, x1, x2)
U25_ggga(x0, x1, x2, x3)
U26_ggga(x0, x1, x2, x3, x4)
U27_ggga(x0, x1, x2, x3, x4)
U28_ggga(x0, x1, x2, x3)

We have to consider all (P,Q,R)-chains.

(47) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(48) TRUE